n:. AtomFree(;n) 

latex

Definitions	Void, a<b, n-m, n+m, -n, #$n, AB, A, False, ij, P  Q, {x:A| B(x) }, x:A. B(x), AtomFree(T;x), x:AB(x), t  T, , s = t, , s ~ t, f(a), x.A(x)
Lemmas	le wf, nat wf, nat properties, ge wf